#!/usr/bin/python
# -*- coding: utf8 -*-

from pyparsing import Literal

from expresion import simpleTypeFactory, atomoFactory
from expresion import Expresion, Tipo, TypeException, Exp, TipoExp, makeSintaxis
from lenguaje import Extension
from booleans import Verdadero, Falso, Boolean


#zero es un valor reduce a se mismo y tipa por defecto:
#vacio | > zero : Nat
Nat = simpleTypeFactory('Nat')
Zero = atomoFactory('zero', Nat)

    
class Succ(Expresion):
    
    def __init__(self, toks):
        """
        Define para estructura succ la expresion que contiene.
        """
        self.termino = toks[0]
               
    def reducir(self):
        """
        Reducir succ(E) corresponde a reducir E.
        """
        terminoRed = self.termino.reducir()
        return Succ([terminoRed])
        
    def tipar(self, namespace):
        """
        gamma | > E : Nat
        -----------------
        gamma | > succ(E) : Nat
        """
        if self.termino.tipar(namespace) == Nat([]):
            return Nat([])
        raise TypeException(('El tipo %s  de la expresion: %s \n'+ \
                            'no se corresponde con el tipo Nat.') % 
                            (self.termino.tipar(namespace), self.termino))
        
    def sustituir(self, var, expresion):
        """
        succ(E) {X <- T} --> succ(E {X <- T})
        """
        return Succ([self.termino.sustituir(var, expresion)])
    
    @classmethod
    def sintaxis(cls):        
        succ = makeSintaxis('succ(', Exp, ')')
        return succ
    
    def __str__(self):
        return "succ(%s)" % self.termino
        

class Pred(Expresion):
    
    def __init__(self, toks):
        """
        Define para estructura succ la expresion que contiene.
        """
        self.termino = toks[0]
    
    def reducir(self):
        """
        Se reduce primero el la expresion que contiene pred, luego:
        pred(zero) --> zero
        pred(succ(v)) --> v
        """
        termino = self.termino.reducir()
        if isinstance(termino, Zero):
            return termino
        else:
            return termino.termino
        
    def tipar(self, namespace):
        """
        gamma | > E : Nat
        -----------------
        gamma | > pred(E) : Nat
        """
        if self.termino.tipar(namespace) == Nat([]):
            return Nat([])
        raise TypeException(('El tipo %s  de la expresion: %s \n'+\
                             'no se corresponde con el tipo Nat.') % 
                             (self.termino.tipar(namespace), self.termino))

    def sustituir(self, var, expresion):
        """
        pred(E) {X <- T} --> pred(E {X <- T})
        """
        return Pred([self.termino.sustituir(var, expresion)])
    
    @classmethod
    def sintaxis(cls):        
        pred = makeSintaxis('pred(', Exp, ')')
        return pred
    
    def __str__(self):
        return "pred(%s)" % self.termino
    
        
class IsZero(Expresion):
    
    def __init__(self, toks):
        """
        Se define para la estructura isZero la expresion que contiene.
        """
        self.termino = toks[0]

    def reducir(self):
        """
        Se reduce primero la expresion que contiene isZero, luego:
        isZero(zero) --> true
        isZero(succ(v)) --> false
        """
        termino = self.termino.reducir()
        if isinstance(termino, Zero):
            return Verdadero([])
        else:
            return Falso([])
        
    def tipar(self, namespace):
        """
        gamma | > E : Nat
        ----------------
        gamma | > isZero(E): Boolean
        """
        if self.termino.tipar(namespace) == Nat([]):
            return Boolean([])
        else:
            raise TypeException(('El tipo %s de la expresion %s no se corresponde con el tipo Nat.') \
                                % (self.termino.tipar(namespace), self.termino))
    
    def sustituir(self, var, expresion):
        """
        isZero(E) {X <- T} --> isZero(E {X <- T})
        """
        return IsZero([self.termino.sustituir(var, expresion)])
    
    @classmethod
    def sintaxis(cls):        
        isZ = makeSintaxis('isZero(', Exp, ')')
        return isZ
    
    def __str__(self):
        return "isZero(%s)" % self.termino

       
extensionNat = Extension('Naturales', 
                         expresiones = [Zero, Succ, Pred, IsZero],
                         tipos = [Nat]
                        )

